Record snapshots in FunctionRecorder with context information#928
Merged
Conversation
There was a problem hiding this comment.
Pull Request Overview
This PR adds context tracking for expression snapshots in the FunctionRecorder and its related translation to correctly handle nested contexts in let‐expressions and quantifiers. Key changes include:
- Introducing a stack of ExpContext in HeapAccessReplacingExpressionTranslator to record let/quantifier scopes.
- Updating the key types in snapshot maps in FunctionRecorder and FunctionData to include context information.
- Adjusting evaluator code to properly push and pop context when evaluating let and quantified expressions.
Reviewed Changes
Copilot reviewed 5 out of 5 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
| src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala | Adds context management and updates getOrFail to use context. |
| src/main/scala/supporters/functions/FunctionRecorder.scala | Integrates context tracking into snapshot recording and adds helper methods to manage the context stack. |
| src/main/scala/supporters/functions/FunctionData.scala | Updates snapshot maps to include context info and adapts call sites accordingly. |
| src/main/scala/rules/Evaluator.scala | Adjusts let & quantifier evaluation to enter and leave the new context. |
| silver | Updates subproject commit. |
Comments suppressed due to low confidence (1)
src/main/scala/supporters/functions/FunctionRecorder.scala:171
- [nitpick] Consider adding a comment clarifying the rationale for using the current '_context' as part of the key when recording snapshots. This can help future maintainers understand why the snapshot is tied to the full context state.
val guardsToSnaps = recordings.getOrElse((loc, _context), InsertionOrderedSet()) + (guards -> snap)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
In particular, remember if snapshots were recorded inside let-expressions or quantifiers, since this can influence the value of the expression and the validity of the guard terms.
We do this by adding a stack of
ExpContexts to the mapping in the FunctionRecorder, which represents the stack of lets and quantifiers inside which an expression's snapshot was recorded. The ExpressionTranslator used to translate function axioms maintains the same kind of stack and looks up expressions in the current context.This fixes #715 and #926.